\begin{tabbing}
fpf{-}sub($A$; $a$.$B$($a$); ${\it eq}$; $f$; $g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$x$:$A$. \+
\\[0ex]($\uparrow$fpf{-}dom(${\it eq}$; $x$; $f$))
\\[0ex]$\Rightarrow$ (($\uparrow$fpf{-}dom(${\it eq}$; $x$; $g$)) c$\wedge$ (fpf{-}ap($f$; ${\it eq}$; $x$) = fpf{-}ap($g$; ${\it eq}$; $x$) $\in$ $B$($x$)))
\-
\end{tabbing}